(set-logic QF_LIA)
(set-info :source |http://www.nec-labs.com/~fsoft/bench.html 
 The following changes have been made: 
 The logic is changed to QF_LIA. 
 The category is set as industrial. 
 The status (except 'large' cases) is assigned according to the 'outfile' on http://www.nec-labs.com/~fsoft/bench.html.  |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun i844 () Int)
(declare-fun i949 () Int)
(declare-fun i1041 () Int)
(declare-fun i1140 () Int)
(declare-fun i1254 () Int)
(declare-fun i1394 () Int)
(declare-fun i1536 () Int)
(declare-fun i1721 () Int)
(declare-fun i1911 () Int)
(assert (let ((?v_12 (+ 0 0))) (let ((?v_204 (= i1721 ?v_12)) (?v_205 (= i1536 ?v_12)) (?v_203 (= i1911 ?v_12))) (let ((?v_208 (ite ?v_203 1 2147483647)) (?v_207 (ite ?v_204 1 2147483647)) (?v_206 (ite ?v_205 1 2147483647)) (?v_201 (+ 1 0))) (let ((?v_0 (= i844 ?v_201))) (let ((?v_1 (ite ?v_0 18 (ite ?v_0 17 22)))) (let ((?v_51 (= ?v_1 (+ 22 0))) (?v_4 (= ?v_1 (+ 18 0)))) (let ((?v_10 (ite (not ?v_4) 0 143)) (?v_2 (ite ?v_4 19 (ite ?v_51 23 ?v_1))) (?v_6 (+ 23 0))) (let ((?v_3 (= ?v_2 ?v_6)) (?v_67 (= ?v_2 (+ 19 0)))) (let ((?v_50 (not ?v_3))) (let ((?v_11 (ite ?v_50 0 ?v_10)) (?v_5 (ite ?v_67 21 (ite ?v_3 25 ?v_2)))) (let ((?v_52 (= ?v_5 (+ 21 0))) (?v_8 (+ 25 0))) (let ((?v_7 (ite (= ?v_5 ?v_8) (ite (not (<= ?v_11 ?v_12)) 30 ?v_5) (ite ?v_52 23 ?v_5))) (?v_16 (+ 30 0))) (let ((?v_14 (= ?v_7 ?v_16)) (?v_9 (= ?v_7 ?v_6))) (let ((?v_47 (ite ?v_9 ?v_10 ?v_11)) (?v_20 (ite (not ?v_14) 0 i949)) (?v_66 (not ?v_9))) (let ((?v_81 (ite ?v_66 0 (ite (not ?v_67) 0 143))) (?v_15 (= ?v_20 ?v_12)) (?v_13 (ite ?v_9 25 (ite ?v_14 32 ?v_7))) (?v_18 (+ 32 0))) (let ((?v_17 (ite (= ?v_13 ?v_8) (ite (not (<= ?v_47 ?v_12)) 30 ?v_13) (ite (not (= ?v_13 ?v_18)) ?v_13 (ite (not ?v_15) 33 (ite ?v_15 222 ?v_13))))) (?v_29 (+ 222 0))) (let ((?v_25 (= ?v_17 ?v_29)) (?v_27 (+ 33 0))) (let ((?v_23 (= ?v_17 ?v_27)) (?v_19 (= ?v_17 ?v_16))) (let ((?v_32 (ite (not ?v_23) 0 i1041)) (?v_38 (ite (not ?v_25) 0 i1041)) (?v_21 (= (ite (not ?v_19) ?v_20 i1041) ?v_12)) (?v_33 (+ 14 0))) (let ((?v_24 (<= ?v_32 ?v_33)) (?v_26 (= ?v_38 ?v_12)) (?v_22 (ite ?v_19 32 (ite ?v_23 35 (ite ?v_25 224 ?v_17)))) (?v_36 (+ 224 0)) (?v_30 (+ 35 0))) (let ((?v_28 (ite (= ?v_22 ?v_18) (ite (not ?v_21) 33 (ite ?v_21 222 ?v_22)) (ite (= ?v_22 ?v_30) (ite ?v_24 36 (ite (not ?v_24) 222 ?v_22)) (ite (not (= ?v_22 ?v_36)) ?v_22 (ite (not ?v_26) 227 (ite ?v_26 242 ?v_22)))))) (?v_45 (+ 242 0))) (let ((?v_48 (= ?v_28 ?v_45)) (?v_44 (+ 227 0)) (?v_43 (+ 36 0))) (let ((?v_40 (= ?v_28 ?v_43)) (?v_37 (= ?v_28 ?v_29)) (?v_31 (= ?v_28 ?v_27))) (let ((?v_56 (ite (not ?v_37) ?v_38 i1140)) (?v_61 (ite (not ?v_40) 0 i1140)) (?v_76 (ite (not ?v_48) 0 i1140)) (?v_34 (<= (ite (not ?v_31) ?v_32 i1140) ?v_33))) (let ((?v_39 (= ?v_56 ?v_12)) (?v_35 (ite ?v_31 35 (ite ?v_37 224 (ite ?v_40 38 (ite (= ?v_28 ?v_44) 229 (ite ?v_48 243 ?v_28)))))) (?v_65 (+ 243 0))) (let ((?v_46 (= ?v_35 ?v_65)) (?v_64 (+ 229 0)) (?v_59 (+ 38 0))) (let ((?v_49 (not ?v_46))) (let ((?v_82 (ite ?v_49 0 ?v_81)) (?v_73 (+ 397 0)) (?v_72 (+ 42 0)) (?v_71 (+ 39 0)) (?v_80 (+ 395 0)) (?v_93 (+ 398 0)) (?v_92 (+ 43 0)) (?v_91 (+ 40 0)) (?v_96 (+ 250 0)) (?v_95 (+ 396 0)) (?v_118 (+ 48 0)) (?v_110 (+ 401 0)) (?v_186 (+ 9 0)) (?v_150 (+ 13 0)) (?v_125 (+ 252 0)) (?v_124 (+ 251 0)) (?v_148 (+ 50 0)) (?v_119 (+ 399 0)) (?v_146 (+ 402 0)) (?v_153 (+ 254 0)) (?v_185 (+ 54 0)) (?v_184 (+ 373 0)) (?v_152 (+ 400 0)) (?v_195 (+ 469 0)) (?v_193 (+ 457 0)) (?v_191 (+ 371 0)) (?v_210 (+ 374 0)) (?v_62 (+ (- 1) 0))) (let ((?v_41 (= ?v_61 ?v_62))) (let ((?v_42 (ite (= ?v_35 ?v_30) (ite ?v_34 36 (ite (not ?v_34) 222 ?v_35)) (ite (= ?v_35 ?v_36) (ite (not ?v_39) 227 (ite ?v_39 242 ?v_35)) (ite (= ?v_35 ?v_59) (ite ?v_41 39 (ite (not ?v_41) 42 ?v_35)) (ite (= ?v_35 ?v_64) 242 (ite ?v_46 397 ?v_35))))))) (let ((?v_55 (= ?v_42 ?v_29)) (?v_60 (= ?v_42 ?v_43)) (?v_75 (= ?v_42 ?v_45)) (?v_86 (= ?v_42 ?v_71)) (?v_128 (= ?v_42 ?v_72)) (?v_53 (ite (not ?v_51) 0 (- 1)))) (let ((?v_77 (ite ?v_66 (ite ?v_50 0 ?v_53) (ite ?v_52 145 ?v_53)))) (let ((?v_78 (ite ?v_49 0 ?v_77)) (?v_143 (ite (not ?v_55) ?v_56 i1254))) (let ((?v_57 (= ?v_143 ?v_12)) (?v_63 (= (ite (not ?v_60) ?v_61 i1254) ?v_62)) (?v_104 (ite (not ?v_75) ?v_76 i1254)) (?v_88 (not ?v_86))) (let ((?v_113 (ite ?v_88 0 ?v_47)) (?v_116 (ite ?v_88 0 ?v_77)) (?v_121 (ite ?v_88 0 ?v_81)) (?v_133 (not ?v_128))) (let ((?v_130 (ite ?v_133 0 ?v_47)) (?v_134 (ite ?v_133 0 ?v_77)) (?v_159 (ite ?v_133 0 ?v_81)) (?v_165 (<= ?v_47 (+ ?v_77 0)))) (let ((?v_194 (not ?v_165)) (?v_170 (ite ?v_204 0 (- 2147483647))) (?v_169 (ite ?v_205 0 (- 2147483647))) (?v_199 (ite ?v_203 0 (- 2147483647))) (?v_68 (ite ?v_49 0 (+ 0 ?v_47 ?v_76)))) (let ((?v_54 (<= ?v_68 (+ ?v_78 0)))) (let ((?v_58 (ite ?v_55 224 (ite ?v_60 38 (ite (= ?v_42 ?v_44) 229 (ite ?v_75 243 (ite ?v_86 40 (ite ?v_128 43 (ite (not (= ?v_42 ?v_73)) ?v_42 (ite (not ?v_54) 398 (ite ?v_54 395 ?v_42))))))))))) (let ((?v_74 (= ?v_58 ?v_65)) (?v_85 (= ?v_58 ?v_91)) (?v_127 (= ?v_58 ?v_92)) (?v_69 (<= ?v_82 (+ ?v_68 0)))) (let ((?v_70 (ite (= ?v_58 ?v_36) (ite (not ?v_57) 227 (ite ?v_57 242 ?v_58)) (ite (= ?v_58 ?v_59) (ite ?v_63 39 (ite (not ?v_63) 42 ?v_58)) (ite (= ?v_58 ?v_64) 242 (ite ?v_74 397 (ite ?v_85 401 (ite ?v_127 48 (ite (= ?v_58 ?v_93) 395 (ite (not (= ?v_58 ?v_80)) ?v_58 (ite (not ?v_69) 396 (ite ?v_69 250 ?v_58)))))))))))) (let ((?v_103 (= ?v_70 ?v_45)) (?v_112 (= ?v_70 ?v_71)) (?v_129 (= ?v_70 ?v_72)) (?v_83 (ite (not ?v_74) ?v_68 (+ 0 ?v_47 ?v_104))) (?v_105 (ite ?v_74 ?v_77 ?v_78))) (let ((?v_79 (<= ?v_83 (+ ?v_105 0))) (?v_107 (ite ?v_74 ?v_81 ?v_82))) (let ((?v_84 (<= ?v_107 (+ ?v_83 0)))) (let ((?v_94 (not ?v_84)) (?v_87 (not ?v_85))) (let ((?v_97 (ite ?v_87 0 ?v_113)) (?v_115 (ite ?v_87 0 ?v_116))) (let ((?v_89 (<= ?v_97 (+ ?v_115 0))) (?v_99 (= ?v_70 ?v_118))) (let ((?v_90 (ite (= ?v_70 ?v_44) 229 (ite ?v_103 243 (ite ?v_112 40 (ite ?v_129 43 (ite (= ?v_70 ?v_73) (ite (not ?v_79) 398 (ite ?v_79 395 ?v_70)) (ite (= ?v_70 ?v_80) (ite ?v_94 396 (ite ?v_84 250 ?v_70)) (ite (= ?v_70 ?v_110) (ite (not ?v_89) 402 (ite ?v_89 399 ?v_70)) (ite ?v_99 50 (ite (= ?v_70 ?v_95) 250 (ite (= ?v_70 ?v_96) 251 ?v_70)))))))))))) (let ((?v_102 (= ?v_90 ?v_65)) (?v_111 (= ?v_90 ?v_91)) (?v_126 (= ?v_90 ?v_92)) (?v_120 (ite ?v_87 0 ?v_121))) (let ((?v_98 (<= ?v_120 (+ ?v_97 0))) (?v_136 (ite (not ?v_99) 0 i1394))) (let ((?v_100 (= ?v_136 ?v_150)) (?v_138 (= ?v_90 ?v_124)) (?v_139 (= ?v_90 ?v_125))) (let ((?v_101 (ite (= ?v_90 ?v_64) 242 (ite ?v_102 397 (ite ?v_111 401 (ite ?v_126 48 (ite (= ?v_90 ?v_93) 395 (ite (= ?v_90 ?v_80) (ite ?v_94 396 (ite ?v_84 250 ?v_90)) (ite (= ?v_90 ?v_95) 250 (ite (= ?v_90 ?v_96) 251 (ite (= ?v_90 ?v_146) 399 (ite (= ?v_90 ?v_119) (ite (not ?v_98) 400 (ite ?v_98 222 ?v_90)) (ite (= ?v_90 ?v_148) (ite ?v_100 373 (ite (not ?v_100) 54 ?v_90)) (ite ?v_138 254 (ite ?v_139 254 ?v_90))))))))))))))) (let ((?v_142 (= ?v_101 ?v_29)) (?v_177 (= ?v_101 ?v_45)) (?v_178 (ite (not ?v_103) ?v_104 i1394))) (let ((?v_108 (ite (not ?v_102) ?v_83 (+ 0 ?v_47 ?v_178))) (?v_179 (ite ?v_102 ?v_77 ?v_105))) (let ((?v_106 (<= ?v_108 (+ ?v_179 0))) (?v_181 (ite ?v_102 ?v_81 ?v_107))) (let ((?v_109 (<= ?v_181 (+ ?v_108 0)))) (let ((?v_145 (not ?v_109)) (?v_114 (not ?v_111))) (let ((?v_122 (ite ?v_114 ?v_97 (ite ?v_112 ?v_47 ?v_113)))) (let ((?v_117 (<= ?v_122 (+ (ite ?v_114 ?v_115 (ite ?v_112 ?v_77 ?v_116)) 0))) (?v_149 (= ?v_101 ?v_118)) (?v_123 (<= (ite ?v_114 ?v_120 (ite ?v_112 ?v_81 ?v_121)) (+ ?v_122 0)))) (let ((?v_147 (not ?v_123)) (?v_154 (= ?v_101 ?v_124)) (?v_155 (= ?v_101 ?v_125)) (?v_131 (not ?v_126)) (?v_132 (not ?v_127))) (let ((?v_160 (ite ?v_131 (ite ?v_132 0 ?v_130) (ite ?v_129 ?v_47 ?v_130)))) (let ((?v_135 (<= ?v_160 (+ (ite ?v_131 (ite ?v_132 0 ?v_134) (ite ?v_129 ?v_77 ?v_134)) 0)))) (let ((?v_162 (not ?v_135)) (?v_137 (= ?v_136 ?v_186)) (?v_168 (not ?v_139))) (let ((?v_156 (ite ?v_138 i1536 (ite ?v_168 0 i1536)))) (let ((?v_140 (<= ?v_156 ?v_12))) (let ((?v_141 (ite ?v_142 224 (ite ?v_177 243 (ite (= ?v_101 ?v_73) (ite (not ?v_106) 398 (ite ?v_106 395 ?v_101)) (ite (= ?v_101 ?v_80) (ite ?v_145 396 (ite ?v_109 250 ?v_101)) (ite (= ?v_101 ?v_110) (ite (not ?v_117) 402 (ite ?v_117 399 ?v_101)) (ite ?v_149 50 (ite (= ?v_101 ?v_95) 250 (ite (= ?v_101 ?v_96) 251 (ite (= ?v_101 ?v_119) (ite ?v_147 400 (ite ?v_123 222 ?v_101)) (ite ?v_154 254 (ite ?v_155 254 (ite (= ?v_101 ?v_152) 222 (ite (= ?v_101 ?v_184) (ite ?v_162 374 (ite ?v_135 371 ?v_101)) (ite (= ?v_101 ?v_185) (ite ?v_137 385 (ite (not ?v_137) 58 ?v_101)) (ite (not (= ?v_101 ?v_153)) ?v_101 (ite ?v_140 457 (ite (not ?v_140) 469 ?v_101))))))))))))))))))) (let ((?v_158 (= ?v_141 ?v_210)) (?v_173 (= ?v_141 ?v_29)) (?v_174 (ite (not ?v_142) ?v_143 i1721))) (let ((?v_144 (= ?v_174 ?v_12)) (?v_176 (= ?v_141 ?v_65)) (?v_163 (ite (not ?v_149) ?v_136 i1721))) (let ((?v_151 (= ?v_163 ?v_150)) (?v_188 (= ?v_141 ?v_124)) (?v_189 (= ?v_141 ?v_125)) (?v_167 (not ?v_155))) (let ((?v_166 (ite ?v_154 i1721 (ite ?v_167 ?v_156 i1721)))) (let ((?v_157 (<= ?v_166 ?v_12)) (?v_161 (<= (ite ?v_131 (ite ?v_132 0 ?v_159) (ite ?v_129 ?v_81 ?v_159)) (+ ?v_160 0)))) (let ((?v_192 (not ?v_161)) (?v_164 (= ?v_163 (+ 5 0))) (?v_198 (ite ?v_154 ?v_170 (ite ?v_167 (ite ?v_138 ?v_169 (ite ?v_168 0 ?v_169)) ?v_170)))) (let ((?v_171 (<= ?v_166 (+ ?v_198 0)))) (let ((?v_172 (ite ?v_173 224 (ite (= ?v_141 ?v_36) (ite (not ?v_144) 227 (ite ?v_144 242 ?v_141)) (ite ?v_176 397 (ite (= ?v_141 ?v_93) 395 (ite (= ?v_141 ?v_80) (ite ?v_145 396 (ite ?v_109 250 ?v_141)) (ite (= ?v_141 ?v_95) 250 (ite (= ?v_141 ?v_96) 251 (ite (= ?v_141 ?v_146) 399 (ite (= ?v_141 ?v_119) (ite ?v_147 400 (ite ?v_123 222 ?v_141)) (ite (= ?v_141 ?v_148) (ite ?v_151 373 (ite (not ?v_151) 54 ?v_141)) (ite ?v_188 254 (ite ?v_189 254 (ite (= ?v_141 ?v_152) 222 (ite (= ?v_141 ?v_153) (ite ?v_157 457 (ite (not ?v_157) 469 ?v_141)) (ite ?v_158 371 (ite (= ?v_141 ?v_191) (ite ?v_192 372 (ite ?v_161 121 ?v_141)) (ite (= ?v_141 (+ 385 0)) (ite ?v_162 386 (ite ?v_135 383 ?v_141)) (ite (= ?v_141 (+ 58 0)) (ite ?v_164 417 (ite (not ?v_164) 62 ?v_141)) (ite (= ?v_141 ?v_193) (ite ?v_194 458 (ite ?v_165 455 ?v_141)) (ite (not (= ?v_141 ?v_195)) ?v_141 (ite (not ?v_171) 470 (ite ?v_171 467 ?v_141))))))))))))))))))))))) (?v_175 (= (ite (not ?v_173) ?v_174 i1911) ?v_12)) (?v_182 (ite (not ?v_176) ?v_108 (+ 0 ?v_47 (ite (not ?v_177) ?v_178 i1721))))) (let ((?v_180 (<= ?v_182 (+ (ite ?v_176 ?v_77 ?v_179) 0))) (?v_183 (<= (ite ?v_176 ?v_81 ?v_181) (+ ?v_182 0))) (?v_187 (= ?v_163 ?v_186)) (?v_197 (not ?v_189))) (let ((?v_196 (ite ?v_188 i1911 (ite ?v_197 ?v_166 i1911)))) (let ((?v_190 (<= ?v_196 ?v_12)) (?v_200 (<= ?v_196 (+ (ite ?v_188 ?v_199 (ite ?v_197 ?v_198 ?v_199)) 0))) (?v_202 (= ?v_163 ?v_201)) (?v_209 (<= (ite ?v_188 ?v_208 (ite ?v_197 (ite ?v_154 ?v_207 (ite ?v_167 (ite ?v_138 ?v_206 (ite ?v_168 0 ?v_206)) ?v_207)) ?v_208)) (+ ?v_196 0)))) (and (and true (not ?v_158)) (= (ite (= ?v_172 ?v_29) 224 (ite (= ?v_172 ?v_36) (ite (not ?v_175) 227 (ite ?v_175 242 ?v_172)) (ite (= ?v_172 ?v_44) 229 (ite (= ?v_172 ?v_45) 243 (ite (= ?v_172 ?v_73) (ite (not ?v_180) 398 (ite ?v_180 395 ?v_172)) (ite (= ?v_172 ?v_80) (ite (not ?v_183) 396 (ite ?v_183 250 ?v_172)) (ite (= ?v_172 ?v_95) 250 (ite (= ?v_172 ?v_96) 251 (ite (= ?v_172 ?v_119) (ite ?v_147 400 (ite ?v_123 222 ?v_172)) (ite (= ?v_172 ?v_124) 254 (ite (= ?v_172 ?v_125) 254 (ite (= ?v_172 ?v_152) 222 (ite (= ?v_172 ?v_184) (ite ?v_162 374 (ite ?v_135 371 ?v_172)) (ite (= ?v_172 ?v_185) (ite ?v_187 385 (ite (not ?v_187) 58 ?v_172)) (ite (= ?v_172 ?v_153) (ite ?v_190 457 (ite (not ?v_190) 469 ?v_172)) (ite (= ?v_172 ?v_191) (ite ?v_192 372 (ite ?v_161 121 ?v_172)) (ite (= ?v_172 ?v_193) (ite ?v_194 458 (ite ?v_165 455 ?v_172)) (ite (= ?v_172 ?v_195) (ite (not ?v_200) 470 (ite ?v_200 467 ?v_172)) (ite (= ?v_172 (+ 372 0)) 121 (ite (= ?v_172 (+ 121 0)) 385 (ite (= ?v_172 (+ 386 0)) 383 (ite (= ?v_172 (+ 383 0)) (ite ?v_192 384 (ite ?v_161 127 ?v_172)) (ite (= ?v_172 (+ 417 0)) (ite ?v_162 418 (ite ?v_135 415 ?v_172)) (ite (= ?v_172 (+ 62 0)) (ite ?v_202 437 (ite (not ?v_202) 66 ?v_172)) (ite (= ?v_172 (+ 458 0)) 455 (ite (= ?v_172 (+ 455 0)) (ite (not (<= ?v_81 (+ ?v_47 0))) 456 ?v_172) (ite (= ?v_172 (+ 470 0)) 467 (ite (not (= ?v_172 (+ 467 0))) ?v_172 (ite (not ?v_209) 468 (ite ?v_209 261 ?v_172)))))))))))))))))))))))))))))) ?v_210))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
